M:Dsys. interface-compatible(M;) 

latex

Definitions	x:A. B(x), interface-compatible(A;B), , P & Q, P  Q, interface-link(A;B;l;tg), , rcv(l,tg) declared in M, mk-ma, , b, x  dom(f), t.1, t.2, deq-member(eq;x;L), reduce(f;k;as), ff, Y, if b then t else f fi , t  T, , x. t(x), Dsys, False, MsgA, Valtype(da;k), x(s)
Lemmas	assert wf, fpf-dom wf, Knd wf, Kind-deq wf, lsrc wf, msga wf, fpf-trivial-subtype-top, rcv wf, false wf, not wf, ldst wf, Id wf, IdLnk wf, dsys wf